The present invention relates to a protocol validation system which receives a specification of a communications protocol, detects an error in the protocol specification and provides a data for correcting the error.
A protocol is a communication agreement among a plurality of communication apparatuses such as an electronic exchange system or terminal system, or among a plurality of logic modules in a communication apparatus. A protocol specification has become complicated, following the latest development of communication technology.
A large scale of software is usually produced by dividing a program into some modules and then combining those modules to achieve a given operation. In this case, a protocol specification must be designed so that there are no errors in a protocol defined between plural modules. Thus, it has become important to design a system such that some communication apparatuses or processes are associated with one another to achieve a given purpose.
In order to establish a design manner of such a system, it is required to clearly describe a requested specification of a protocol specification and then validate whether there is an error in the requested specification or not. An error or redundancy in the requested specification can be removed by analyzing an informal request for a protocol specification and then describing the requested specification formally. Thus, removal of an error or redundancy makes it possible to show a protocol specification clearly and to test it automatically. If a software designer detects an error in a protocol specification at the stage of its design, operation fed back from the development or maintenance stage of a software to the design stage of a protocol specification would be avoided. Therefore, the detection of an error at the design stage of a protocol specification makes it possible to enhance productivity of software.
Recently, two types of protocol validation systems have been reported.
One prior validation system is such that for a protocol having a plurality of processes, a system state is defined as the combination of a state of each process and a state on each channel between processes, and all the states reachable from an initial state are enumerated, or subsets necessary to detect validity items are enumerated--see, for example, C. H. West, "General technique for communications protocol validation", IBM J. Res, Devel., July 1978.
Alternatively, the other type of a prior validation system is such that all the system states are not enumerated, but an excutable state transition provided by transmission or reception of one signal in each process is expanded like a tree in accordance with a condition which regulates that a message is transmitable or receivable at a state in each process, and that an error is found on a process of expansition; for example, D. Brand and P. Zafiropulo, "On communicating finite-state machine", IBM Res. Rep. RZ1053, 1981.
The present invention relates to the latter type of protocol validation system in which validity is effected for each process. Therefore, this type of prior protocol validation system will be now described below, referring to FIGS. 1 and 2. FIG. 1 shows an example of a protocol to be tested. This protocol is a communication system with processes 1, 2 and 3. Each of the processes 1 and 3 may be a terminal apparatus and process 2 may be an exchange system, or all the processes 1, 2 and 3 may be included in a single CPU. A process is defined as a processing unit which performs a signal transmission and/or a signal reception between the other processes of different functions. A communication system is composed of a plurality of processes. Therefore, the protocol of FIG. 1 shows a communication system composed of three processes.
In FIG. 1, a circle shows a state of a process, and an arrow shows a state transition. Labels -x and +x attached to an arrow show transmission and reception of a signal x, respectively. An initial state of each process is 1. Therefore, it will be understood from FIG. 1 that the state of the process 1 changes from the initial state 1 to the state 2 when the process 1 sends a signal 1 to the process 2, or changes from 1 to 3 when it receives a signal 3 from the process 2, or changes from 1 to 2 when it receives a signal 6 from the process 3. Likewise, the other processes 2 and 3 operate. Although an operation of each process is simple, it is difficult to find a logical error in an operation between processes.
FIGS. 2(a) through 2(c) show a result obtained by applying the latter prior validation system mentioned above to the protocol of FIG. 1. FIGS. 2a), 2(b) and 2(c) show expansion of state transitions of the processes 1, 2 and 3, respectively, and are thus called a state transition expansion chart. A system state is shown by attaching to a state of one considered process states of other processes which must reach so that said state of said considered process is obtained. A set of those states is called a L value at a state in a considered process.
The description will be now given of a drawing manner of a state transition expansion chart as well as a calculation manner of a L value at each state for the protocol of FIG. 1. Although a state name and a signal name use those shown in FIG. 1 for convenience in the following description, in order to distinguish a state name or a signal name which appear more than two times from those which appear first, after ".", the numeral 0 is provided when those appear first, the numeral 1 is provided when those appear secondly, the numeral 2 is provided when those appear thirdly, and so on. For example, 2.1 shows the state 2 which appears secondly, or the signal 2 which appears secondly. Thus, such a numeral after "." suggests the number of times a state or a signal occurs.
First, the initial state of each process is 1, and thus .circle.1.0 is drawn for each process and the L value at the state 1 of each process is initiated as (1.0 1.0 1.0). For example, in the L value (1.0 1.0 1.0) at the state 1.0 of the process 1, the first element 1.0 shows that the state of the process 1 itself is 1, the second element 1.0 shows that the process 1 knows that the state of the process 2 is 1, and the third element 1.0 shows that the process 1 knows that the state of the process 3 is 1. At this time, an executable transmission transition is -1 in the process 1 or -3 in the process 2. For execution of the transmission transition -1 in the process 1, an arrow with the label -1.0 and .circle.2.0 are drawn as shown in FIG. 2(a). The L value at the state 2.0 of the process 1 is set as (2.0 1.0 1.0), because the process 1 does not know changes of states of the processes 2 and 3 corresponding to the transmission of the signal 1.0. The first element of that L value shows the state of the process 1 itself is 2. The reception transition +1.0 in the process 2 corresponding to the transmission transition -1.0 is then executed. For this execution, an arrow with the label + 1.0 and .circle.2.0 is drawn as shown in FIG. 2(b). The process 2 can know that the state of the process 1 is 2 by the reception of the signal 1.0. However, the process 2 does not know a change of a state of the process 3, and thus the L value at the state 2.0 of the process 2 is set as (2.0 2.0 1.0), in which the second element 2.0 shows that the state of the process 2 itself is 2.
For execution of the transmission transition -3 in the process 2, an arrow with the label -3.0 and .circle.3.0 are drawn as shown in FIG. 2(b). The L value at the state 3.0 of the process 2 is provided as (1.0 3.0 1.0), since the process 2 does not know change of states in the processes 1 and 3 resulting from the transmission of the signal 3.0. At this time, the process 2 recognizes that the state of the process 1 after execution of this transmission transition -3.0 is 1. It is thus understood that the transmission transition -1.0 in the process 1 is executable at the state 1.0 of the process 1, and thus the reception transition +1.0 corresponding to that transmission transition -1.0 is executable at the state 3.0 of the process 2. Therefore, it is tried to draw an arrow with the label +1.0 at the state 3.0. However, as is apparent from FIG. 1, the reception transition +1 is not defined, but executable at the state 3 of the process 2. As a result, the reception transition +1.0 at the state 3.0 of the process 2 is detected as an unspecified executable transition. This unspecified executable transition is indicated, as shown in FIG. 2(b), by a dotted arrow with the label +1.0 in the chart.
Next, the reception transition +3.0 in the process 1 corresponding to the transmission transition -3.0 in the process 2 is executed. For this execution, an arrow with the label +3.0 and .circle.3.0 are drawn as shown in FIG. 2(a). Then process 1 does not know a change of a state in the process 3. Therefore, the L value at the state 3.0 of the process 1 is (3.0 3.0 1.0), in which the first element 3.0 shows that the state of the process 1 itself is 3. At this system state, it is understood that the state 2.0 of the process 1 can receive the signal 3.0 sent from the process 2, since the transmission transition -1.0 from the state 1.0 to the state 2.0 in the process 2 has already been executed. Thus, it is tried to draw an arrow with the label 3.0 at the state 2.0 of the process 1. However, the reception transition +3 is not defined at the state 2 of the process 1 in the protocol of FIG. 1. Therefore, this reception transition +3.0 is detected as an unspecified executable transition and is then drawn by a dotted arrow with the label +3.0 as shown in FIG. 2(a).
At this time, executable transmission transitions are -2, -5 in the process 1 and -4 in the process 2. For execution of the transmission transition -5 in the process 1, an arrow with the label -5.0 and .circle.4.0 are drawn as shown in FIG. 2(a). The L value at this state is provided as (4.0 1.0 1.0). The reception transition +5.0 in the process 3 corresponding to the transmission transition -5.0 in the process 1 is then executed. For this execution, an arrow with the label +5.0 and .circle.2.0 are drawn as shown in FIG. 2(c). The L value at this state is (4.0 1.0 2.0). At this time, the transmission transition -6 in the process 3 is executable. For this execution, an arrow with the label -6.0 and .circle.1.1 are drawn as shown in FIG. 2(c). The L value at this state is (4.0 1.0 1.1). It will be understood that at this time, states of the processes 1, 2 and 3 are 4.0, 2.0 and 1.1, respectively, and that no signal on channels exists (, which means all the transmission signals have been received), and no executable transmission transition and no executable reception transition exist. Such a system state is detected as a deadlock. It should be noted that the state of the process 2 is not 1.0 which is shown in that L value but 2.0, because the reception transition +1.0 in the process 2, which correspondings to the transmission transition -1.0 in the process 1, has already executed. Further, at the state 4.1 of the process 1, the reception transition +6 is never executed, unless the transmission transition -6 in the process 3 is executed. Therefore, it is understood that in expansion of state transitions mentioned above, the reception transition +6 expanded in sequence from the state 1.0 of the process 1 is unexecutable, or is never executed. Such a state transition is detected as a specified unexecutable transition.
According to the above-mentioned manner, state transitions in each process are expanded, and thus the protocol of FIG. 1 is expanded as shown in FIGS. 2(a) through 2(c).
The description will be now given of a stop manner for stopping expansion of a state transition.
As shown in FIG. 2(a), the L value at the state 2.1 of the process 1 is (2.1 2.1 1.0) and the L value at the state 2.4 of the process 1 is (2.4 2.4 1.0). That is, two system states are the same. It is thus understood that state transitions -2, +4 between states 2.1 and 2.4 of the process 1 are repeated from the state 2.4. As a result, expansion is stopped at the state 2.4. As mentioned later, at this time we say that the state 2.4 is marked by type 1. Likewise, expansion is stopped at the states 2.6, 4.1, 4.3, 4.5, 4.7 and 4.8 in the process 1, as well as the states 3.4 and 3.6 in the process 2.
The state 3.4 in the process 1 can receive only the signal 4 which is sent from the state 3.4 in the process 2. However, the expansion from the state 3.4 of the process 2 has been already stopped. Thus, the expansion from the state 3.4 of the process 1 is stopped. As mentioned later, at this time, we say that the state 3.4 of the proces 1 is marked by type 1. Likewise, the expansion from the state 2.4 in the process 2 is stopped.
The expansion from the state 1.1 of the process 3 is stopped, since the state 4.1 of the process 1, the state 2.0 of the process 2 and the state 1.1 of the process 3 are a deadlock state. Likewise, the expansions from the states 1.2, 1.3, 1.4 and 1.5 of the process 3 are stopped.
However, a prior protocol validation system thus describes has the disadvantage that a large amount of handling time makes difficult the validity test, when a protocol is large and complicated with many states and transitions, since all the state transition sequences in each process are enumerated and the conditions for stopping the expansion are not severe. The prior system has another disadvantage that it has not been implemented by hardware yet, because it needs a large scale of memory for storing the state transition chart.